es:event_system{i:l}, i:Id, ds:fpf(Id; x.Type).
@i discrete ds  subtype_rel(es-state(es; i); decl-state(ds)) 

latex

Definitions	ff, tt, if b then t else f fi , prop{i:l}, top, fpf-cap(f; eq; x; z), x. t(x), t  T, P  Q, x:A. B(x), P  Q, Unit, , P  Q, es-dtype(es; i; x; T), fpf-all(A; eq; f; x,v.P(x;v)), @i discrete ds, x(s),
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, es-vartype wf, not wf, bnot wf, assert wf, bool wf, fpf-trivial-subtype-top, fpf-dom wf, event system wf, Id wf, fpf wf, es-dds wf, id-deq wf, fpf-sub weakening, vartype-es-state-sub